perm filename LISP.AX[F76,JMC] blob sn#249278 filedate 1976-11-23 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE INDVAR X Y Z
C00003 00003	AXIOM CONS:
C00004 00004	AXIOM APPEND:
C00005 ENDMK
C⊗;
DECLARE INDVAR X Y Z;
DECLARE OPCONST CAR CDR 1 [R←700];
DECLARE OPCONST CONS 2;
DECLARE PREDCONST ATOM NULL 1 [R←700];
DECLARE OPCONST * 2 [INF];

DECLARE PREDPAR P 1;

DECLARE INDCONST NILL;
AXIOM CONS:
	∀X Y.(CAR CONS(X,Y) = X)
	∀X Y.(CDR CONS(X,Y) = Y)
	∀X.(¬ATOM X ⊃ CONS(CAR X,CDR X) = X)
	∀X Y.¬ATOM CONS(X,Y)
;;

AXIOM INDUCTION:
	∀X.(ATOM X ∨ P(CAR X) ∧ P(CDR X) ⊃ P(X)) ⊃ ∀X.P(X)
	∀X.(NULL X ∨ P(CDR X) ⊃ P(X)) ⊃ ∀X.P(X)
;;

AXIOM LIST:
	¬NULL CONS(X,Y)
	NULL NILL
	ATOM NILL
;;

AXIOM NULL:
	∀X.(NULL X ≡ X = NILL)
;;
AXIOM APPEND:
	∀X Y.(X * Y = IF NULL X THEN Y ELSE CONS(CAR X, CDR X * Y))
;;